(set-option :produce-interpolants true)
(set-logic QF_LRA)
(declare-fun |x#0| () Real)
(declare-fun |x#0##0| () Real)
(declare-fun |x#0##1| () Real)
(declare-fun |ts::x0##0| () Real)
(declare-fun |ts::x0##1| () Real)
(declare-fun |ts::x0##2| () Real)
(assert
(let ((?def206 (and (<= 0 (* (- 1) |ts::x0##1|))
 (<= 0 |ts::x0##1|)
)))
(let ((?def198 (and (<= (- 10) (* (- 1) |ts::x0##0|))
 (<= 10 |ts::x0##0|)
)))
(let ((?def204 (not ?def198)))
(let ((?def207 (or ?def204 ?def206)))
(let ((?def202 (and (<= (- 1) (+ |ts::x0##0| (* (- 1) |ts::x0##1|)))
 (<= 1 (+ (* (- 1) |ts::x0##0|) |ts::x0##1|))
)))
(let ((?def203 (or ?def198 ?def202)))
(let ((?def208 (and ?def203 ?def207)))
(let ((?def167 (and (<= 0 |ts::x0##2|)
 (<= 0 (* (- 1) |ts::x0##2|))
)))
(let ((?def154 (and (<= (- 10) (* (- 1) |ts::x0##1|))
 (<= 10 |ts::x0##1|)
)))
(let ((?def164 (not ?def154)))
(let ((?def168 (or ?def164 ?def167)))
(let ((?def162 (and (<= (- 1) (+ |ts::x0##1| (* (- 1) |ts::x0##2|)))
 (<= 1 (+ (* (- 1) |ts::x0##1|) |ts::x0##2|))
)))
(let ((?def163 (or ?def154 ?def162)))
(let ((?def169 (and ?def163 ?def168)))
(let ((?def209 (and ?def169 ?def208)))

?def209
))))))))))))))))
(push 1)
(assert
(let ((?def0 true))

?def0
))
(push 1)
(assert
(let ((?def174 (and (<= 0 |ts::x0##0|)
 (<= 0 (* (- 1) |ts::x0##0|))
)))
(let ((?def137 (not (<= (- 10) (* (- 1) |ts::x0##2|)))))
(let ((?def175 (and ?def137 ?def174)))

?def175
))))
(check-sat)
(pop 1)
(check-sat)
(exit)
